------------- MODULE ralR2 -------------

EXTENDS Naturals, Sequences, TLC

CONSTANT L, \* décomposition binaire maximale de l'ensemble
         D  \* type des �l�ments

ASSUME L \geq 1

CHOIX == { "Insert", "Remove", "Put", "Get", "Occurrence", "Cardinal" }

ELT == INSTANCE skew WITH P <- L, D <- D

\* Sequence avec le poids le plus faible en tete.
ETAT == [ liste:[ 1..L -> ELT!ETAT ], has2:BOOLEAN]

Inv(etat) ==
 /\ etat \in ETAT

Zero == << >>

\*---------------------------------------------------------------

Insert[d \in ELT!ETAT, liste \in Seq(ELT!ETAT), b \in BOOLEAN] ==
	IF liste = Zero THEN
		[result |-> <<d>>, 
		 carry  |-> FALSE]
	ELSE
		CASE b		-> 
					CASE Head(liste) = ELT!VIDE			-> [result |-> ELT!Join(<<ELT!VIDE>>, Insert[d, Tail(liste), b].result),
															carry  |-> Insert[d, Tail(liste), b].carry]
					[] Head(Tail(liste)) /= ELT!VIDE	-> [result |-> ELT!Join(<<ELT!VIDE>>, ELT!Join(<<ELT!Join(d, ELT!Join(Head(liste), Head(Tail(liste)))), Tail(Tail(liste)))),
															carry  |-> TRUE]
					[] OTHER							-> [result |-> ELT!Join(<<ELT!VIDE>>, ELT!Join(<<ELT!Join(d, Head(liste))>>, Tail(Tail(liste)))),
															carry  |-> FALSE]
		[] OTHER	-> 
					CASE Head(liste) = ELT!VIDE		-> [result |-> ELT!Join(<< d >>, Tail(liste)),
														carry  |-> FALSE]
					[] OTHER						-> [result |-> ELT!Join(<<ELT!Join(d, Head(liste))>>, Tail(liste)),
														carry  |-> TRUE]

\*---------------------------------------------------------------

Remove[liste \in Seq(ELT!ETAT), b \in BOOLEAN] ==
	CASE (Len(ss) = 1)	-> [result |-> <<ELT!VIDE>>,
							borrow |-> Head(ss),
							bool   |-> FALSE]
	[] OTHER			-> 
/* Ex : 101, 001, ...
						CASE (Head(liste) /= ELT!VIDE) -> [result |-> <<ELT!Pick2(Head(liste)).deck>> \o Tail(liste),
														   borrow |-> ELT!Pick2(Head(liste)).card,
														   carry  |-> FALSE]
/* Ex : 120, ...
						[] (Head(liste) = ELT!VIDE /\ b = TRUE /\ Head(Tail(liste)) /= ELT!VIDE)	->
							LET s = ELT!Split(Head(Tail(liste))) IN
														  [result |-> <<ELT!Pick2(s[1]).deck>> \o <<s[2]>> \o Tail(Tail(liste)),
														   borrow |-> ELT!Pick2(s[1]).card,
														   carry  |-> TRUE]
/* Ex : 110, 210, 10.
						[] (Head(liste) = ELT!VIDE /\ b = FALSE /\ Head(Tail(liste)) /= ELT!VIDE)	->
														[result |-> <<ELT!Pick2(s[1]).deck>> \o <<ELT!VIDE>> \o Tail(Tail(liste)),
														 borrow |-> ELT!Pick2(s[1]).card,
														 carry  |-> TRUE]
/* Ex : 100, 200, 0
						[] (Head(liste) = ELT!VIDE /\ Head(Tail(liste)) = ELT!VIDE)					->
							LET remove_succ == Remove[Tail(liste), b] IN
														[result |-> <<Head(liste)>> \o remove_succ.result,
														 borrow |-> remove_succ.borrow,
														 carry  |-> remove_succ.carry]

\*---------------------------------------------------------------

PutAux[ss \in ELT!ETAT, n \in Nat, d \in D, tailleAux \in Nat] ==
	LET s == ELT!Split(ss) IN
	LET div == tailleAux \div 2 IN
		CASE s[1] = ELT!Vide -> ELT!Unit(d)
		[] s[2] = ELT!Vide   -> ELT!Unit(d)
		[] n <= div          -> PutAux[s[1], n, d, div] \o s[2]
		[] tailleAux % 2 = 0 -> s[1] \o PutAux[s[2], n-div, d, div]
		[] OTHER             -> s[1] \o PutAux[s[2], n-div, d, div+1]



Put[i \in Nat, elt \in D, liste \in Seq(ELT!ETAT), b \in BOOLEAN] ==
	LET Put2 [i2 \in Nat, elt2 \in D, liste2 \in Seq(ELT!ETAT), k \in Nat, taille \in Nat, b2 \in BOOLEAN] ==
		CASE (Head(liste2) = ELT!VIDE) -> [result |-> ELT!Join(<<Head(liste2)>>, PutAux[i2, elt2, Tail(liste2), k, taille*2, b2].result),
										   carry  |-> b2]
/* Pas de 2, donc taille de la case = 2^i-1										
		[] b2 = FALSE /\ i2 \in k+1 .. k+taille-1	-> [result |-> ELT!Join(<<PutAux[Head(liste2), i2-k, elt2, taille-1]>>, Tail(liste2)),
														carry  |-> b2]
/* On arrive au 2, taille de la case = (2^(i-1)-1)*2
		[] b2 = TRUE /\ i2 \in k+1 .. k+(taille-1)*2	-> [result |-> ELT!Join(<<PutAux[Head(liste2), i2-k, elt2, (taille-1)*2]>>, Tail(liste2)),
															carry  |-> b2]

		[] b2 = TRUE -> [result |-> ELT!Join(<<Head(liste2)>>, Put2[i2-k, elt2, Tail(liste2), k+(taille-1)*2, taille*2, FALSE].result),
						 carry  |-> b2]

		[] b2 = FALSE -> [result |-> ELT!Join(<<Head(liste2)>>,Put2[i2-k, elt2, Tail(liste2), k+taille-1, taille*2, FALSE].result,

						  carry  |-> b2]
	IN Put2[i, elt, liste, 0, 2, b]


\*---------------------------------------------------------------

GetAux[ss \in ELT!ETAT, n \in Nat, tailleAux \in Nat] ==
	LET s == ELT!Split(ss) IN
	LET div == tailleAux \div 2 IN
		CASE s[1] = ELT!Vide -> Head(s[2])
		[]   s[2] = ELT!Vide -> Head(s[1])
		[]   n <= div -> GetAux[s[1], n, div]
		[]   tailleAux % 2 = 0 -> GetAux[s[2], n-div, div]
		[]   OTHER             -> GetAux[s[2], n-div, div+1]


Get[i \in Nat, liste \in Seq(ELT!ETAT), b \in BOOLEAN] ==
	LET Get2 [i2 \in Nat, liste2 \in Seq(ELT!ETAT), k \in Nat, case \in Nat, b2 \in BOOLEAN] ==
		CASE (Head(liste2) = ELT!Vide)				-> Get2[i2, Tail(liste2), k, case*2, b2]

		[] b2 = FALSE /\ i2 \in k+1 .. k+case-1		-> GetAux[Head(liste2), i2-k, case-1]

		[] b2 = TRUE  /\ i2 \in k+1 .. k+(case-1)*2	-> GetAux[Head(liste2), i2-k, (case-1)*2]

		[] b2 = TRUE								-> Get2[i2-k, Tail(liste2), k+(case-1)*2, case*2, FALSE]

		[] b2 = FALSE -> Get2[i2-k, Tail(liste2), k+case-1, case*2, FALSE]

	IN Get2[i, liste, 0, 2, b]

\*---------------------------------------------------------------

\* Occurrence 				  
Occurrence[ss \in Seq(ELT!ETAT), elt \in D] ==
	LET Aux[s \in Seq(ELT!ETAT), cpt \in Nat] ==
		CASE (s = Zero)		-> cpt
		[] OTHER			-> Aux[Tail(s), cpt + ELT!Occurrence(Head(s), elt)]
	IN Aux[ss, 0]

\*---------------------------------------------------------------

Cardinal[ss \in Seq(ELT!ETAT), b \in BOOLEAN] ==
	LET Aux[s \in Seq(ELT!ETAT), bAux \in BOOLEAN, elt \in Nat, cpt \in Nat] ==
		CASE (s = Zero) -> elt
		[] (Head(s) = ELT!VIDE) -> Aux[Tail(s), bAux, elt, cpt*2]
		[] bAux = FALSE -> Aux[Tail(s), bAux, elt+cpt-1, cpt*2]
		[] OTHER	-> Aux[Tail(s), FALSE, elt+(cpt-1)*2, cpt*2]
	IN Aux[ss, b, 0, 2]

\*---------------------------------------------------------------

\* �tat initial
Init(etat) ==
 /\ etat = [ liste |-> [ i \in 1..L |-> ELT!VIDE ], b |-> FALSE ]

\* incr�menter
Pre_Insert(param, etat) ==
 /\ param \in D
 /\ etat.liste[L] = ELT!Vide

Act_Insert(param, etat, etat_p, result) ==
 LET inc == Insert[ELT!Unit(param), etat.liste, etat.b] IN
 /\ etat_p = [liste |-> inc.result, b |-> inc.carry]
 /\ result = "__NO_DATA"

\* d�cr�menter
Pre_Remove(param, etat) ==
 /\ param = "__NO_DATA"
 /\ \E i \in 1..L : etat.liste[i] # ELT!Vide

Act_Remove(param, etat, etat_p, result) ==
 LET dec == Remove[etat.liste, etat.b] IN
 /\ etat_p = [liste |-> dec.result, b |-> dec.carry]
 /\ result = dec.borrow

\* Put
Pre_Put(param, etat) ==
 /\ param \in [ indice : 1..Cardinal[etat.liste, etat.b], valeur : D ]
 /\ etat /= Zero

Act_Put(param, etat, etat_p, result) ==
 LET inc == Put[param.indice, param.valeur, etat.liste, etat.b] IN
 /\ etat_p = [liste |-> inc.result, b |-> inc.carry]
 /\ result = "__NO_DATA"

\* Get
Pre_Get(param, etat) ==
 /\ param \in 1..Cardinal[etat.liste, etat.b]
 
Act_Get(param, etat, etat_p, result) ==
LET dec == Get[param, etat.liste, etat.b] IN
 /\ etat_p = etat
 /\ result = dec

\* cardinal
Pre_Cardinal(param, etat) ==
 /\ param = "__NO_DATA"

Act_Cardinal(param, etat, etat_p, result) ==
 /\ etat_p = etat
 /\ result = Cardinal[etat.liste, etat.b]
 
 \* occurrence
Pre_Occurrence(param, etat) ==
 /\ param \in D

Act_Occurrence(param, etat, etat_p, result) ==
LET oc == Occurrence[param, etat.liste, etat.b] IN
 /\ etat_p = etat
 /\ result = oc
                                  
-------------------------------------------

ContratClient(choix, param, etat) ==
 \/ (choix = "Insert"     /\ Pre_Insert(param, etat))
 \/ (choix = "Remove"     /\ Pre_Remove(param, etat))
 \/ (choix = "Put"        /\ Pre_Put(param, etat))
 \/ (choix = "Get"        /\ Pre_Get(param, etat))
 \/ (choix = "Occurrence" /\ Pre_Occurrence(param, etat))
 \/ (choix = "Cardinal"   /\ Pre_Cardinal(param, etat))

ContratModule(choix, param, etat, etat_prime, result) ==
 /\ (choix = "Insert"     => (Pre_Insert(param, etat)     => Act_Insert(param, etat, etat_prime, result)))
 /\ (choix = "Remove"     => (Pre_Remove(param, etat)     => Act_Remove(param, etat, etat_prime, result)))
 /\ (choix = "Put"        => (Pre_Put(param, etat)        => Act_Put(param, etat, etat_prime, result)))
 /\ (choix = "Get"        => (Pre_Get(param, etat)        => Act_Get(param, etat, etat_prime, result)))
 /\ (choix = "Occurrence" => (Pre_Occurrence(param, etat) => Act_Occurrence(param, etat, etat_prime, result)))
 /\ (choix = "Cardinal"   => (Pre_Cardinal(param, etat)   => Act_Cardinal(param, etat, etat_prime, result)))

===========================================
